Erasure-Illegal-Access.agda:4,10-11
Variable x is declared erased, so it cannot be used here
when checking that the expression x has type A
